Nuprl Lemma : eqmod_functionality_wrt_eqmod
2,24
postcript
pdf
m
,
m'
,
a
,
a'
,
b
,
b'
:
.
m
=
m'
(
a
=
a'
mod
m
)
(
b
=
b'
mod
m
)
((
a
=
b
mod
m
)
(
a'
=
b'
mod
m'
))
latex
Definitions
P
Q
,
P
&
Q
,
P
Q
,
P
Q
,
a
=
b
mod
m
,
x
:
A
.
B
(
x
)
,
Prop
,
t
T
Lemmas
eqmod
transitivity
,
eqmod
inversion
,
eqmod
wf
origin